YES(O(1),O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { f(0()) -> 1()
  , f(s(x)) -> g(x, s(x))
  , g(0(), y) -> y
  , g(s(x), y) -> g(x, s(+(y, x)))
  , g(s(x), y) -> g(x, +(y, s(x)))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs:
  { f(s(x)) -> g(x, s(x))
  , g(s(x), y) -> g(x, s(+(y, x)))
  , g(s(x), y) -> g(x, +(y, s(x)))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y)) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
      [f](x1) = 3*x1 + x1^2     
                                
        [0]() = 0               
                                
        [1]() = 0               
                                
      [s](x1) = 1 + x1          
                                
  [g](x1, x2) = 3*x1 + x1^2 + x2
                                
  [+](x1, x2) = 1 + x1 + 2*x2   
                                
  
  This order satisfies the following ordering constraints.
  
        [f(0())] =                    
                 >=                   
                 =  [1()]             
                                      
       [f(s(x))] =  4 + 5*x + x^2     
                 >  4*x + x^2 + 1     
                 =  [g(x, s(x))]      
                                      
     [g(0(), y)] =  y                 
                 >= y                 
                 =  [y]               
                                      
    [g(s(x), y)] =  4 + 5*x + x^2 + y 
                 >  5*x + x^2 + 2 + y 
                 =  [g(x, s(+(y, x)))]
                                      
    [g(s(x), y)] =  4 + 5*x + x^2 + y 
                 >  5*x + x^2 + 3 + y 
                 =  [g(x, +(y, s(x)))]
                                      
     [+(x, 0())] =  1 + x             
                 >  x                 
                 =  [x]               
                                      
    [+(x, s(y))] =  3 + x + 2*y       
                 >  2 + x + 2*y       
                 =  [s(+(x, y))]      
                                      

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { f(0()) -> 1()
  , g(0(), y) -> y }
Weak Trs:
  { f(s(x)) -> g(x, s(x))
  , g(s(x), y) -> g(x, s(+(y, x)))
  , g(s(x), y) -> g(x, +(y, s(x)))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs: { g(0(), y) -> y }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
      [f](x1) = 3*x1 + x1^2       
                                  
        [0]() = 0                 
                                  
        [1]() = 0                 
                                  
      [s](x1) = 1 + x1            
                                  
  [g](x1, x2) = 2 + x1 + x1^2 + x2
                                  
  [+](x1, x2) = 1 + x1 + x2       
                                  
  
  This order satisfies the following ordering constraints.
  
        [f(0())] =                    
                 >=                   
                 =  [1()]             
                                      
       [f(s(x))] =  4 + 5*x + x^2     
                 >  3 + 2*x + x^2     
                 =  [g(x, s(x))]      
                                      
     [g(0(), y)] =  2 + y             
                 >  y                 
                 =  [y]               
                                      
    [g(s(x), y)] =  4 + 3*x + x^2 + y 
                 >= 4 + 2*x + x^2 + y 
                 =  [g(x, s(+(y, x)))]
                                      
    [g(s(x), y)] =  4 + 3*x + x^2 + y 
                 >= 4 + 2*x + x^2 + y 
                 =  [g(x, +(y, s(x)))]
                                      
     [+(x, 0())] =  1 + x             
                 >  x                 
                 =  [x]               
                                      
    [+(x, s(y))] =  2 + x + y         
                 >= 2 + x + y         
                 =  [s(+(x, y))]      
                                      

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs: { f(0()) -> 1() }
Weak Trs:
  { f(s(x)) -> g(x, s(x))
  , g(0(), y) -> y
  , g(s(x), y) -> g(x, s(+(y, x)))
  , g(s(x), y) -> g(x, +(y, s(x)))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs: { f(0()) -> 1() }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
      [f](x1) = 3*x1 + x1^2   
                              
        [0]() = 1             
                              
        [1]() = 1             
                              
      [s](x1) = 1 + x1        
                              
  [g](x1, x2) = x1 + x1^2 + x2
                              
  [+](x1, x2) = x1 + 2*x2     
                              
  
  This order satisfies the following ordering constraints.
  
        [f(0())] =  4                 
                 >  1                 
                 =  [1()]             
                                      
       [f(s(x))] =  4 + 5*x + x^2     
                 >  2*x + x^2 + 1     
                 =  [g(x, s(x))]      
                                      
     [g(0(), y)] =  2 + y             
                 >  y                 
                 =  [y]               
                                      
    [g(s(x), y)] =  2 + 3*x + x^2 + y 
                 >  3*x + x^2 + 1 + y 
                 =  [g(x, s(+(y, x)))]
                                      
    [g(s(x), y)] =  2 + 3*x + x^2 + y 
                 >= 3*x + x^2 + y + 2 
                 =  [g(x, +(y, s(x)))]
                                      
     [+(x, 0())] =  x + 2             
                 >  x                 
                 =  [x]               
                                      
    [+(x, s(y))] =  x + 2 + 2*y       
                 >  1 + x + 2*y       
                 =  [s(+(x, y))]      
                                      

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { f(0()) -> 1()
  , f(s(x)) -> g(x, s(x))
  , g(0(), y) -> y
  , g(s(x), y) -> g(x, s(+(y, x)))
  , g(s(x), y) -> g(x, +(y, s(x)))
  , +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^2))